Ad hoc networks are formed as collections of nodes that communicate over wireless channels. The dynamic and distributed nature of such networks means that randomization is often used to improve efficiency and to achieve symmetric solutions. In this talk, we demonstrate the applicability of an automated formal verification technique called probabilistic model checking to the analysis of ad hoc network protocols. A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. Probabilistic specifications typically express statements such as 'is leader election eventually resolved with probability 1?', 'what is the expected time to deliver one message?', and 'what is the probability that the message will be delivered within 30ms?'. The usefulness of the techniques will be demonstrated through a number of case studies analyzing real-world protocols performed with PRISM, a probabilistic symbolic model checker developed at the University of Birmingham (www.cs.bham.ac.uk/~dxp/prism/). Examples will include the Zeroconf dynamic configuration protocol for IPv4 link-local addresses and Bluetooth device discovery.